Close the Section 8 physical-fibre and all-deficit seam - #45

Purpose

This draft PR is the closure-focused implementation stacked on PR #44. It targets the one remaining submission-blocking seam identified by the full TeX re-audit:

attained physical high skeletons
  <-> block support + admissible deficits + local partial stub matchings,

with exact weight preservation.

The branch starts from agent/625-full-tex-mathematical-reaudit, so it contains the theorem-upgrade dossier, the full TeX re-audit, the exact endpoint reference normalization from PR #41, the decorated-to-physical injection, and the repaired q-only Section IX frontier.

Planned theorem chain

The PR will advance only through focused, warning-fatal Lean checkpoints.

1. Validate and repair Section8EndpointPhysicalReverseData.lean.
2. Prove the reverse endpoint map and both round trips, yielding an equivalence

   FourEndpointDecoratedBlockPairing ≃ FourEndpointPhysicalFibre.
   

3. Define the literal partial-cell physical matching fibre for multiplicity j=m-h and prove its exact cardinality.
4. Prove the aggregate local weight identity

   w(P,j)
     = product_e (s_e)_{j_e}(t_e)_{j_e}/j_e!
       * product_e g(j_e) / (n)_J.
   

5. Prove a disjoint reindexing of every attained canonical high physical skeleton by block support, deficits, and local partial matchings.
6. Establish the global comparison

   w(P,m-h)/w_full(P)
     <= product_e n^(h_e) R_{m_e,d_e}(h_e),
   

   with

   R_{m,d}(h)
     = C(m,h)/((d+1)...(d+h)) * 2^(-hm+h(h+1)/2).
   

7. Apply the existing all-high geometric product and endpoint transport to obtain the bare-skeleton estimate at scale exp(o(n/(log n)^4)).
8. Compose with the existing q-only literal attachment theorem to expose Proposition 9.2 from one explicit Section VIII theorem.

Current first checkpoint

The first commit adds a dedicated Lean 4.31 workflow that:

• rejects sorry, admit, sorryAx, project-defined axioms/constants, and unsafe declarations in every closure module;
• builds the deepest closure module currently present under --wfail;
• uploads the exact compiler log.

The initial target is the inherited candidate reverse-data construction. It is not counted as proved until this focused workflow is green.

Scope boundary

This PR must remain draft until each claimed theorem has a green focused build and an explicit axiom audit. At creation time it does not prove the endpoint equivalence, the partial-cell fibre, the global all-deficit reindexing, Lemma 8.3, Proposition 9.2, or Erdos625Statement.